1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Gluing metric spaces
5 Authors: Sébastien Gouëzel
6 -/
7
8 import topology.metric_space.isometry topology.metric_space.premetric_space
src └────────────────────────────┘ └───────────────────────────────────┘
9
10 /-!
11 # Metric space gluing
12
13 Gluing two metric spaces along a common subset. Formally, we are given
14
15 ```
16 Φ
17 γ ---> α
18 |
19 |Ψ
20 v
21 β
22 ```
23 where `hΦ : isometry Φ` and `hΨ : isometry Ψ`.
24 We want to complete the square by a space `glue_space hΦ hΨ` and two isometries
25 `to_glue_l hΦ hΨ` and `to_glue_r hΦ hΨ` that make the square commute.
26 We start by defining a predistance on the disjoint union `α ⊕ β`, for which
27 points `Φ p` and `Ψ p` are at distance 0. The (quotient) metric space associated
28 to this predistance is the desired space.
29
30 This is an instance of a more general construction, where `Φ` and `Ψ` do not have to be isometries,
31 but the distances in the image almost coincide, up to `2ε` say. Then one can almost glue the two
32 spaces so that the images of a point under `Φ` and `Ψ` are ε-close. If `ε > 0`, this yields a
33 metric space structure on `α ⊕ β`, without the need to take a quotient. In particular, when
34 `α` and `β` are inhabited, this gives a natural metric space structure on `α ⊕ β`, where the basepoints
35 are at distance 1, say, and the distances between other points are obtained by going through the
36 two basepoints.
37
38 We also define the inductive limit of metric spaces. Given
39 ```
40 f 0 f 1 f 2 f 3
41 X 0 -----> X 1 -----> X 2 -----> X 3 -----> ...
42 ```
43 where the `X n` are metric spaces and `f n` isometric embeddings, we define the inductive
44 limit of the `X n`, also known as the increasing union of the `X n` in this context, if we
45 identify `X n` and `X (n+1)` through `f n`. This is a metric space in which all `X n` embed
46 isometrically and in a way compatible with `f n`.
47
48 -/
49
50 noncomputable theory
51
52 universes u v w
53 variables {α : Type u} {β : Type v} {γ : Type w}
54
55 open function set premetric lattice
56
57 namespace metric
58 section approx_gluing
59
60 variables [metric_space α] [metric_space β]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
61 {Φ : γ → α} {Ψ : γ → β} {ε : ℝ}
id ┴
src ┴
typ ┴
62 open lattice
63 open sum (inl inr)
64
65 /-- Define a predistance on α ⊕ β, for which Φ p and Ψ p are at distance ε -/
66 def glue_dist (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) : α ⊕ β → α ⊕ β → ℝ
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
67 | (inl x) (inl y) := dist x y
id ┴ └─┘ ┴ └──┘
src └─┘ └──┘
typ ┴ └─┘ ┴ └──┘
68 | (inr x) (inr y) := dist x y
id ┴ └─┘ ┴ └──┘
src └─┘ └──┘
typ ┴ └─┘ ┴ └──┘
69 | (inl x) (inr y) := infi (λp, dist x (Φ p) + dist y (Ψ p)) + ε
id └─┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ └──┘ └──┘ ┴ └──┘ ┴
typ └─┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
70 | (inr x) (inl y) := infi (λp, dist y (Φ p) + dist x (Ψ p)) + ε
id └─┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └─┘ └─┘ └──┘ └──┘ ┴ └──┘ ┴
typ └─┘ ┴ └─┘ ┴ └──┘ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
71
72 private lemma glue_dist_self (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) : ∀x, glue_dist Φ Ψ ε x x = 0
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
73 | (inl x) := dist_self _
id └─┘ └───────┘
src └─┘ └───────┘
typ └─┘ └───────┘
74 | (inr x) := dist_self _
id └─┘ └───────┘
src └─┘ └───────┘
typ └─┘ └───────┘
75
76 lemma glue_dist_glued_points [nonempty γ] (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) (p : γ) :
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
77 glue_dist Φ Ψ ε (inl (Φ p)) (inr (Ψ p)) = ε :=
id └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └───────┘ └─┘ └─┘ ┴
typ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
doc └───────┘
78 begin
79 have : infi (λq, dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q)) = 0,
id └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └─────┘└──┘┴ └─┘ ┴ ┴ └┘ ┴ └┘┴┴└──┘┴ ┴ └┘ ┴ └─┘┴└┘
typ └─────┘└──┘┴ └─┘ ┴ ┴ └┘ ┴┴ └┘┴┴└──┘┴ ┴┴└┘ ┴┴ └─┘┴└┘
doc └─────┘└──┘┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘
txt └─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘
par └─────┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ └┘
pid └───┘└┘ ┴ └─┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └─┘ ┴┴
st └────────────────────────────────────────────────┘└─
80 { have A : ∀q, 0 ≤ dist (Φ p) (Φ q) + dist (Ψ p) (Ψ q) :=
id ┴ ┴ └──┘ ┴ ┴
src └───────┘ ┴ └─┘┴┴ ┴ ┴ └┘ ┴ └┘ ┴└──┘┴ ┴ └┘ ┴ └────
typ └───────┘ ┴ └─┘┴┴ ┴ ┴ └┘ ┴┴ └┘ ┴└──┘┴ ┴┴└┘ ┴┴ └────
doc └───────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └────
txt └───────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └────
par └───────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └────
pid └────┘└─┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴└───
st ───┘└───────────────────────────────────────────────────────
81 λq, by rw ← add_zero (0 : ℝ); exact add_le_add dist_nonneg dist_nonneg,
id └──────┘ └────────┘ └─────────┘
src ─────┘ └─┘ ┴└───┘└──────┘┴ └──┘ ┴└┘└────┘└────────┘┴ ┴└─────────┘
typ ─────┘ └─┘ ┴└───┘└──────┘┴ └──┘ ┴└┘└────┘└────────┘┴ ┴└─────────┘
doc ─────┘ └─┘ ┴└───┘ ┴ └──┘ ┴└┘└────┘ ┴ ┴
txt ─────┘ └─┘ ┴└───┘ ┴ └──┘ ┴└┘└────┘ ┴ ┴
par ─────┘ └─┘ ┴└───┘ ┴ └──┘ ┴└┘└────┘ ┴ ┴
pid ─────┘ └─┘ └────┘ ┴ └──┘ └───────┘ ┴ ┴
st ───────────┘└──────────────────────────────────────────────────────────────┘└─
82 refine le_antisymm _ (le_cinfi A),
id └─────────┘ └──────┘ ┴
src └─────┘└─────────┘└─┘ └──────┘┴ ┴
typ └─────┘└─────────┘└─┘ └──────┘┴┴┴
doc └─────┘ └─┘ └──────┘┴ ┴
txt └─────┘ └─┘ ┴ ┴
par └─────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────────────────────┘└─
83 have : 0 = dist (Φ p) (Φ p) + dist (Ψ p) (Ψ p), by simp,
id ┴ └──┘ ┴ ┴
src └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴└──┘┴ ┴ └┘ ┴ ┴ └──┘
typ └───────┘ ┴ ┴ ┴ └┘ ┴┴ └┘ ┴└──┘┴ ┴ └┘ ┴┴┴┴ └──┘
doc └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
txt └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
par └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴ └──┘
pid └───┘└──┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ ┴
st ─────────────────────────────────────────────────┘ └─
84 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
85 exact cinfi_le ⟨0, forall_range_iff.2 A⟩ },
id └──────┘ └──────────────┘ ┴
src └────┘└──────┘┴ └─┘└──────────────┘└─┘ └┘
typ └────┘└──────┘┴ └─┘└──────────────┘└─┘┴└┘
doc └────┘└──────┘┴ └─┘ └─┘ └┘
txt └────┘ ┴ └─┘ └─┘ └┘
par └────┘ ┴ └─┘ └─┘ └┘
pid ┴ ┴ └─┘ └─┘ ┴┴
st ────────────────────────────────────────────┘└┘└
86 rw [glue_dist, this, zero_add]
id └───────┘ └──┘ └──────┘
src └──┘└───────┘└┘ └┘└──────┘└┘
typ └──┘└───────┘└┘└──┘└┘└──────┘└┘
doc └──┘└───────┘└┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ──────────────┘└────┘└────────┘┴┴
87 end
st └─┘
88
89 private lemma glue_dist_comm (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
90 ∀x y, glue_dist Φ Ψ ε x y = glue_dist Φ Ψ ε y x
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
91 | (inl x) (inl y) := dist_comm _ _
id └─┘ └───────┘
src └─┘ └───────┘
typ └─┘ └───────┘
92 | (inr x) (inr y) := dist_comm _ _
id └─┘ └───────┘
src └─┘ └───────┘
typ └─┘ └───────┘
93 | (inl x) (inr y) := rfl
id └─┘ └─┘ └─┘
src └─┘ └─┘ └─┘
typ └─┘ └─┘ └─┘
94 | (inr x) (inl y) := rfl
id └─┘ └─┘ └─┘
src └─┘ └─┘ └─┘
typ └─┘ └─┘ └─┘
95
96 variable [nonempty γ]
id └──────┘
src └──────┘
typ └──────┘
97
98 private lemma glue_dist_triangle (Φ : γ → α) (Ψ : γ → β) (ε : ℝ)
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
99 (H : ∀p q, abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε) :
id ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ └──┘ ┴ └──┘ ┴ ┴
typ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
100 ∀x y z, glue_dist Φ Ψ ε x z ≤ glue_dist Φ Ψ ε x y + glue_dist Φ Ψ ε y z
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘ └───────┘
101 | (inl x) (inl y) (inl z) := dist_triangle _ _ _
id └─┘ └───────────┘
src └─┘ └───────────┘
typ └─┘ └───────────┘
102 | (inr x) (inr y) (inr z) := dist_triangle _ _ _
id └─┘ └───────────┘
src └─┘ └───────────┘
typ └─┘ └───────────┘
103 | (inr x) (inl y) (inl z) := begin
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
st └─────
104 have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id └───────┘ └───┘ ┴ ┴ ┴ └──┘ ┴
src └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘┴┴└──┘┴ ┴ ┴ └──────
typ └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘┴└─┘ ┴ ┴ ┴┴ └┘┴┴└──┘┴ ┴ ┴┴ └──────
doc └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
txt └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
par └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
pid └────┘└─┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘└───
st ─────────────────────────────────────────────────────────────────────────────────
105 λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id └──────────────┘ └────────┘ └─────────┘
src ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
typ ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
doc ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
txt ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
par ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
pid ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
106 unfold glue_dist,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───────────────────┘└─
107 have : infi (λp, dist z (Φ p) + dist x (Ψ p)) ≤ infi (λp, dist y (Φ p) + dist x (Ψ p)) + dist y z,
id ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘┴┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘┴┴└──┘┴ └─┘ ┴ ┴ ┴┴ └┘ ┴ ┴┴┴ ┴┴ └─┘ ┴└──┘┴┴┴┴
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
108 { have : infi (λp, dist y (Φ p) + dist x (Ψ p)) + dist y z =
id ┴
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴└
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴┴└
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
st ─────┘└──────────────────────────────────────────────────────────
109 infi ((λt, t + dist y z) ∘ (λp, dist y (Φ p) + dist x (Ψ p))),
id └──┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘┴┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘
typ ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴┴└┘┴┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘
doc ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
txt ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
par ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
pid ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
110 { refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λt, t + dist y z)) _ (B _ _),
id └──────────────────────────────────────┘ └────────┘ └──┘ ┴ ┴ ┴
src └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴└──┘┴ ┴ └───┘ └───┘
typ └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴└──┘┴┴┴┴└───┘ ┴└───┘
doc └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
txt └─────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
par └─────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
pid ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
st ───────┘└───────────────────────────────────────────────────────────────────────────────────────────┘└─
111 exact continuous_id.add continuous_const,
id └───────────────┘ └──────────────┘
src └────┘└───────────────┘┴└──────────────┘
typ └────┘└───────────────┘┴└──────────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────────────┘└─
112 exact λx y hx, by simpa },
src └────┘ └──────┘ ┴└────┘
typ └────┘ └──────┘ ┴└────┘
doc └────┘ └──────┘ ┴└────┘
txt └────┘ └──────┘ ┴└────┘
par └────┘ └──────┘ ┴└────┘
pid ┴ └──────┘ └─────┘
st ────────────────────────┘└─────┘└┘└
113 rw [this, comp],
id └──┘ └──┘
src └──┘ └┘└──┘┴
typ └──┘└──┘└┘└──┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────┘└────┘└──
114 refine cinfi_le_cinfi (B _ _) (λp, _),
id └────────────┘ ┴
src └─────┘└────────────┘┴ └────┘ └───┘
typ └─────┘└────────────┘┴ ┴└────┘ └───┘
doc └─────┘└────────────┘┴ └────┘ └───┘
txt └─────┘ ┴ └────┘ └───┘
par └─────┘ ┴ └────┘ └───┘
pid ┴ ┴ └────┘ └───┘
st ──────────────────────────────────────────┘└─
115 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────────
116 dist z (Φ p) + dist x (Ψ p) ≤ (dist y z + dist y (Φ p)) + dist x (Ψ p) :
st ─────────────────────────────────────────────────────────────────────────────────
117 add_le_add (dist_triangle_left _ _ _) (le_refl _)
id └────────┘ └────────────────┘ └─────┘
src └────────┘ └────────────────┘ └─────┘
typ └────────┘ └────────────────┘ └─────┘
st ────────────────────────────────────────────────────────────
118 ... = dist y (Φ p) + dist x (Ψ p) + dist y z : by ring },
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────────────────────────────────────────────────┘└────┘└┘└
119 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────
120 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
121 | (inr x) (inr y) (inl z) := begin
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
st └─────
122 have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id └───────┘ └───┘ ┴ ┴ └──┘ ┴
src └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └──────
typ └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘┴└─┘ ┴ ┴ ┴┴ └┘ ┴└──┘┴ ┴ ┴┴ └──────
doc └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
txt └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
par └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
pid └────┘└─┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘└───
st ─────────────────────────────────────────────────────────────────────────────────
123 λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id └──────────────┘ └────────┘ └─────────┘
src ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
typ ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
doc ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
txt ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
par ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
pid ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
124 unfold glue_dist,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───────────────────┘└─
125 have : infi (λp, dist z (Φ p) + dist x (Ψ p)) ≤ dist x y + infi (λp, dist z (Φ p) + dist y (Ψ p)),
id ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴┴┴ ┴ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └┘
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
126 { have : dist x y + infi (λp, dist z (Φ p) + dist y (Ψ p)) =
src └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
par └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
st ─────┘└──────────────────────────────────────────────────────────
127 infi ((λt, dist x y + t) ∘ (λp, dist z (Φ p) + dist y (Ψ p))),
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘
typ ───────────┘└──┘┴ └─┘ ┴┴┴ ┴ ┴ └┘ ┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘
doc ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
txt ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
par ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
pid ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
128 { refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λt, dist x y + t)) _ (B _ _),
id └──────────────────────────────────────┘ └────────┘ └──┘ ┴ ┴ ┴
src └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘└──┘┴ ┴ ┴ ┴ └───┘ └───┘
typ └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘└──┘┴┴┴┴┴ ┴ └───┘ ┴└───┘
doc └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
txt └─────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
par └─────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
pid ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
st ───────┘└───────────────────────────────────────────────────────────────────────────────────────────┘└─
129 exact continuous_const.add continuous_id,
id └──────────────────┘ └───────────┘
src └────┘└──────────────────┘┴└───────────┘
typ └────┘└──────────────────┘┴└───────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────────────┘└─
130 exact λx y hx, by simpa },
src └────┘ └──────┘ ┴└────┘
typ └────┘ └──────┘ ┴└────┘
doc └────┘ └──────┘ ┴└────┘
txt └────┘ └──────┘ ┴└────┘
par └────┘ └──────┘ ┴└────┘
pid ┴ └──────┘ └─────┘
st ────────────────────────┘└─────┘└┘└
131 rw [this, comp],
id └──┘ └──┘
src └──┘ └┘└──┘┴
typ └──┘└──┘└┘└──┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────┘└────┘└──
132 refine cinfi_le_cinfi (B _ _) (λp, _),
id └────────────┘ ┴
src └─────┘└────────────┘┴ └────┘ └───┘
typ └─────┘└────────────┘┴ ┴└────┘ └───┘
doc └─────┘└────────────┘┴ └────┘ └───┘
txt └─────┘ ┴ └────┘ └───┘
par └─────┘ ┴ └────┘ └───┘
pid ┴ ┴ └────┘ └───┘
st ──────────────────────────────────────────┘└─
133 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────────
134 dist z (Φ p) + dist x (Ψ p) ≤ dist z (Φ p) + (dist x y + dist y (Ψ p)) :
st ─────────────────────────────────────────────────────────────────────────────────
135 add_le_add (le_refl _) (dist_triangle _ _ _)
id └────────┘ └─────┘ └───────────┘
src └────────┘ └─────┘ └───────────┘
typ └────────┘ └─────┘ └───────────┘
st ───────────────────────────────────────────────────────
136 ... = dist x y + (dist z (Φ p) + dist y (Ψ p)) : by ring },
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────────────────────────────────────────────────────┘└────┘└┘└
137 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────
138 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
139 | (inl x) (inl y) (inr z) := begin
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
st └─────
140 have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id └───────┘ └───┘ ┴ ┴ └──┘ ┴
src └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └──────
typ └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘┴└─┘ ┴ ┴ ┴┴ └┘ ┴└──┘┴ ┴ ┴┴ └──────
doc └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
txt └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
par └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
pid └────┘└─┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘└───
st ─────────────────────────────────────────────────────────────────────────────────
141 λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id └──────────────┘ └────────┘ └─────────┘
src ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
typ ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
doc ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
txt ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
par ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
pid ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
142 unfold glue_dist,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───────────────────┘└─
143 have : infi (λp, dist x (Φ p) + dist z (Ψ p)) ≤ dist x y + infi (λp, dist y (Φ p) + dist z (Ψ p)),
id ┴ └──┘ ┴ ┴ └──┘ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └┘
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴┴┴ ┴ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └┘
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
144 { have : dist x y + infi (λp, dist y (Φ p) + dist z (Ψ p)) =
src └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
typ └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
doc └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
par └─────┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ └
st ─────┘└──────────────────────────────────────────────────────────
145 infi ((λt, dist x y + t) ∘ (λp, dist y (Φ p) + dist z (Ψ p))),
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘
typ ───────────┘└──┘┴ └─┘ ┴┴┴ ┴ ┴ └┘ ┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘
doc ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
txt ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
par ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
pid ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
146 { refine cinfi_of_cinfi_of_monotone_of_continuous ( _ : continuous (λt, dist x y + t)) _ (B _ _),
id └──────────────────────────────────────┘ └────────┘ └──┘ ┴ ┴ ┴
src └─────┘└──────────────────────────────────────┘┴ └───┘└────────┘┴ └─┘└──┘┴ ┴ ┴ ┴ └───┘ └───┘
typ └─────┘└──────────────────────────────────────┘┴ └───┘└────────┘┴ └─┘└──┘┴┴┴┴┴ ┴ └───┘ ┴└───┘
doc └─────┘└──────────────────────────────────────┘┴ └───┘└────────┘┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
txt └─────┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
par └─────┘ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
pid ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
st ───────┘└────────────────────────────────────────────────────────────────────────────────────────────┘└─
147 exact continuous_const.add continuous_id,
id └──────────────────┘ └───────────┘
src └────┘└──────────────────┘┴└───────────┘
typ └────┘└──────────────────┘┴└───────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────────────┘└─
148 exact λx y hx, by simpa },
src └────┘ └──────┘ ┴└────┘
typ └────┘ └──────┘ ┴└────┘
doc └────┘ └──────┘ ┴└────┘
txt └────┘ └──────┘ ┴└────┘
par └────┘ └──────┘ ┴└────┘
pid ┴ └──────┘ └─────┘
st ────────────────────────┘└─────┘└┘└
149 rw [this, comp],
id └──┘ └──┘
src └──┘ └┘└──┘┴
typ └──┘└──┘└┘└──┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────┘└────┘└──
150 refine cinfi_le_cinfi (B _ _) (λp, _),
id └────────────┘ ┴
src └─────┘└────────────┘┴ └────┘ └───┘
typ └─────┘└────────────┘┴ ┴└────┘ └───┘
doc └─────┘└────────────┘┴ └────┘ └───┘
txt └─────┘ ┴ └────┘ └───┘
par └─────┘ ┴ └────┘ └───┘
pid ┴ ┴ └────┘ └───┘
st ──────────────────────────────────────────┘└─
151 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────────
152 dist x (Φ p) + dist z (Ψ p) ≤ (dist x y + dist y (Φ p)) + dist z (Ψ p) :
st ─────────────────────────────────────────────────────────────────────────────────
153 add_le_add (dist_triangle _ _ _) (le_refl _)
id └────────┘ └───────────┘ └─────┘
src └────────┘ └───────────┘ └─────┘
typ └────────┘ └───────────┘ └─────┘
st ───────────────────────────────────────────────────────
154 ... = dist x y + (dist y (Φ p) + dist z (Ψ p)) : by ring },
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────────────────────────────────────────────────────┘└────┘└┘└
155 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────
156 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
157 | (inl x) (inr y) (inr z) := begin
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
st └─────
158 have B : ∀a b, bdd_below (range (λ (p : γ), dist a (Φ p) + dist b (Ψ p))) :=
id └───────┘ └───┘ ┴ ┴ └──┘ ┴
src └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └──────
typ └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘┴└─┘ ┴ ┴ ┴┴ └┘ ┴└──┘┴ ┴ ┴┴ └──────
doc └───────┘ └─┘ ┴└───────┘┴ └───┘┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
txt └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
par └───────┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──────
pid └────┘└─┘ └─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘└───
st ─────────────────────────────────────────────────────────────────────────────────
159 λa b, ⟨0, forall_range_iff.2 (λp, add_nonneg dist_nonneg dist_nonneg)⟩,
id └──────────────┘ └────────┘ └─────────┘
src ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
typ ─────┘ └───┘ └─┘└──────────────┘└─┘ └─┘└────────┘┴ ┴└─────────┘└┘
doc ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
txt ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
par ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
pid ─────┘ └───┘ └─┘ └─┘ └─┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────────────────────────┘└─
160 unfold glue_dist,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ───────────────────┘└─
161 have : infi (λp, dist x (Φ p) + dist z (Ψ p)) ≤ infi (λp, dist x (Φ p) + dist y (Ψ p)) + dist y z,
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘┴ ┴
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴ ┴ ┴ ┴┴ └─┘ ┴└──┘┴┴┴┴
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
162 { have : infi (λp, dist x (Φ p) + dist y (Ψ p)) + dist y z =
src └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
typ └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
doc └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
txt └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
par └─────┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
pid └───┘└┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └
st ─────┘└──────────────────────────────────────────────────────────
163 infi ((λt, t + dist y z) ∘ (λp, dist x (Φ p) + dist y (Ψ p))),
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘
typ ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴┴└┘ ┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘
doc ───────────┘└──┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
txt ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
par ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
pid ───────────┘ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
164 { refine cinfi_of_cinfi_of_monotone_of_continuous (_ : continuous (λt, t + dist y z)) _ (B _ _),
id └──────────────────────────────────────┘ └────────┘ └──┘ ┴ ┴ ┴
src └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴└──┘┴ ┴ └───┘ └───┘
typ └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴└──┘┴┴┴┴└───┘ ┴└───┘
doc └─────┘└──────────────────────────────────────┘┴ └──┘└────────┘┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
txt └─────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
par └─────┘ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
pid ┴ ┴ └──┘ ┴ └─┘ ┴ ┴ ┴ ┴ └───┘ └───┘
st ───────┘└───────────────────────────────────────────────────────────────────────────────────────────┘└─
165 exact continuous_id.add continuous_const,
id └───────────────┘ └──────────────┘
src └────┘└───────────────┘┴└──────────────┘
typ └────┘└───────────────┘┴└──────────────┘
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────────────┘└─
166 exact λx y hx, by simpa },
src └────┘ └──────┘ ┴└────┘
typ └────┘ └──────┘ ┴└────┘
doc └────┘ └──────┘ ┴└────┘
txt └────┘ └──────┘ ┴└────┘
par └────┘ └──────┘ ┴└────┘
pid ┴ └──────┘ └─────┘
st ────────────────────────┘└─────┘└┘└
167 rw [this, comp],
id └──┘ └──┘
src └──┘ └┘└──┘┴
typ └──┘└──┘└┘└──┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ─────────────┘└────┘└──
168 refine cinfi_le_cinfi (B _ _) (λp, _),
id └────────────┘ ┴
src └─────┘└────────────┘┴ └────┘ └───┘
typ └─────┘└────────────┘┴ ┴└────┘ └───┘
doc └─────┘└────────────┘┴ └────┘ └───┘
txt └─────┘ ┴ └────┘ └───┘
par └─────┘ ┴ └────┘ └───┘
pid ┴ ┴ └────┘ └───┘
st ──────────────────────────────────────────┘└─
169 calc
id └──┘
src └──┘
typ └──┘
doc └──┘
st ───────────
170 dist x (Φ p) + dist z (Ψ p) ≤ dist x (Φ p) + (dist y z + dist y (Ψ p)) :
st ─────────────────────────────────────────────────────────────────────────────────
171 add_le_add (le_refl _) (dist_triangle_left _ _ _)
id └────────┘ └─────┘ └────────────────┘
src └────────┘ └─────┘ └────────────────┘
typ └────────┘ └─────┘ └────────────────┘
st ────────────────────────────────────────────────────────────
172 ... = dist x (Φ p) + dist y (Ψ p) + dist y z : by ring },
id ┴ ┴ ┴ ┴ └──┘ ┴ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────────────────────────────────────────────────┘└────┘└┘└
173 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────
174 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
175 | (inl x) (inr y) (inl z) := real.le_of_forall_epsilon_le $ λδ δpos, begin
id └─┘ └─┘ └──────────────────────────┘ ┴ └──┘
src └─┘ └─┘ └──────────────────────────┘
typ └─┘ └─┘ └──────────────────────────┘ ┴ └──┘
st └─────
176 have : ∃a ∈ range (λp, dist x (Φ p) + dist y (Ψ p)), a < infi (λp, dist x (Φ p) + dist y (Ψ p)) + δ/2 :=
id ┴ └───┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴┴
src └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘ ┴ ┴└────
typ └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘ ┴┴┴└────
doc └─────┘ └──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
txt └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
par └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
pid └───┘└┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
177 exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id └──────────────────┘ └────────────┘ └──┘
src ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
typ ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
doc ─────┘└──────────────────┘┴ └──┘ ┴└──┘└──┘┴└┘└──────┘┴
txt ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
par ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
pid ─────┘ ┴ └──┘ └───┘ └──────────┘
st ────────────────────────────────────────────────┘└───────┘┴└────────┘┴└─
178 rcases this with ⟨a, arange, ha⟩,
id └──┘
src └─────┘ └───────────────────┘
typ └─────┘└──┘└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ───────────────────────────────────┘└─
179 rcases mem_range.1 arange with ⟨p, pa⟩,
id └───────┘ └────┘
src └─────┘└───────┘└─┘ └───────────┘
typ └─────┘└───────┘└─┘└────┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────────────┘└─
180 rw ← pa at ha,
id └┘
src └───┘ └────┘
typ └───┘└┘└────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ └────┘
st ────────────────┘└─
181 have : ∃b ∈ range (λp, dist z (Φ p) + dist y (Ψ p)), b < infi (λp, dist z (Φ p) + dist y (Ψ p)) + δ/2 :=
id ┴ └───┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘ ┴ └────
typ └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘ ┴┴ └────
doc └─────┘ └──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
txt └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
par └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
pid └───┘└┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
182 exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id └──────────────────┘ └────────────┘ └──┘
src ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
typ ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
doc ─────┘└──────────────────┘┴ └──┘ ┴└──┘└──┘┴└┘└──────┘┴
txt ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
par ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
pid ─────┘ ┴ └──┘ └───┘ └──────────┘
st ────────────────────────────────────────────────┘└───────┘┴└────────┘┴└─
183 rcases this with ⟨b, brange, hb⟩,
id └──┘
src └─────┘ └───────────────────┘
typ └─────┘└──┘└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ───────────────────────────────────┘└─
184 rcases mem_range.1 brange with ⟨q, qb⟩,
id └───────┘ └────┘
src └─────┘└───────┘└─┘ └───────────┘
typ └─────┘└───────┘└─┘└────┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────────────┘└─
185 rw ← qb at hb,
id └┘
src └───┘ └────┘
typ └───┘└┘└────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ └────┘
st ────────────────┘└─
186 have : dist (Φ p) (Φ q) ≤ dist (Ψ p) (Ψ q) + 2 * ε,
id ┴ └──┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └┘ ┴ └┘ ┴└──┘┴ ┴ └┘ ┴ └┘ └─┘ ┴
typ └─────┘ ┴ ┴ └┘ ┴┴ └┘ ┴└──┘┴ ┴┴└┘ ┴┴┴└┘ └─┘ ┴┴
doc └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
par └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
st ─────────────────────────────────────────────────────┘└─
187 { have := le_trans (le_abs_self _) (H p q), by linarith },
id └──────┘ └─────────┘ ┴ ┴ ┴
src └──────┘└──────┘┴ └─────────┘└──┘ ┴ ┴ ┴ └───────┘
typ └──────┘└──────┘┴ └─────────┘└──┘ ┴┴┴┴┴┴ └───────┘
doc └──────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘
par └──────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘
pid └───┘└─┘ ┴ └──┘ ┴ ┴ ┴ ┴
st ───────┘└──────────────────────────────────────┘ └┘└
188 calc dist x z ≤ dist x (Φ p) + dist (Φ p) (Φ q) + dist (Φ q) z : dist_triangle4 _ _ _ _
id └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └────────────┘
src └──┘ └──┘ └────────────┘
typ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └────────────┘
doc └──┘
st ────────────────────────────────────────────────────────────────────────────────────────────
189 ... ≤ dist x (Φ p) + dist (Ψ p) (Ψ q) + dist z (Φ q) + 2 * ε : by rw [dist_comm z]; linarith
id ┴ ┴ └───────┘ ┴
src └──┘└───────┘┴ ┴ └────────
typ ┴ ┴ └──┘└───────┘┴┴┴ └────────
doc └──┘ ┴ ┴ └────────
txt └──┘ ┴ ┴ └────────
par └──┘ ┴ ┴ └────────
pid └┘ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────┘└──────────────┘┴└──────────
190 ... ≤ dist x (Φ p) + (dist y (Ψ p) + dist y (Ψ q)) + dist z (Φ q) + 2 * ε :
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└───────────────────────────────────────────────────────────────────────────
191 add_le_add (add_le_add (add_le_add (le_refl _) (dist_triangle_left _ _ _)) (le_refl _)) (le_refl _)
id └────────┘ └────────────────┘ └─────┘
src └────────┘ └────────────────┘ └─────┘
typ └────────┘ └────────────────┘ └─────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────
192 ... ≤ (infi (λp, dist x (Φ p) + dist y (Ψ p)) + ε) + (infi (λp, dist z (Φ p) + dist y (Ψ p)) + ε) + δ :
id ┴ └──┘ ┴ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴ ┴
doc └──┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
193 by linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────┘└─────────
194 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
195 | (inr x) (inl y) (inr z) := real.le_of_forall_epsilon_le $ λδ δpos, begin
id └─┘ └─┘ └──────────────────────────┘ ┴ └──┘
src └─┘ └─┘ └──────────────────────────┘
typ └─┘ └─┘ └──────────────────────────┘ ┴ └──┘
st └─────
196 have : ∃a ∈ range (λp, dist y (Φ p) + dist x (Ψ p)), a < infi (λp, dist y (Φ p) + dist x (Ψ p)) + δ/2 :=
id ┴ └───┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘ ┴ └────
typ └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘ ┴┴ └────
doc └─────┘ └──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
txt └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
par └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
pid └───┘└┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
197 exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id └──────────────────┘ └────────────┘ └──┘
src ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
typ ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
doc ─────┘└──────────────────┘┴ └──┘ ┴└──┘└──┘┴└┘└──────┘┴
txt ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
par ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
pid ─────┘ ┴ └──┘ └───┘ └──────────┘
st ────────────────────────────────────────────────┘└───────┘┴└────────┘┴└─
198 rcases this with ⟨a, arange, ha⟩,
id └──┘
src └─────┘ └───────────────────┘
typ └─────┘└──┘└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ───────────────────────────────────┘└─
199 rcases mem_range.1 arange with ⟨p, pa⟩,
id └───────┘ └────┘
src └─────┘└───────┘└─┘ └───────────┘
typ └─────┘└───────┘└─┘└────┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────────────┘└─
200 rw ← pa at ha,
id └┘
src └───┘ └────┘
typ └───┘└┘└────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ └────┘
st ────────────────┘└─
201 have : ∃b ∈ range (λp, dist y (Φ p) + dist z (Ψ p)), b < infi (λp, dist y (Φ p) + dist z (Ψ p)) + δ/2 :=
id ┴ └───┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─┘ ┴ └────
typ └─────┘┴└──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘┴┴ ┴ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─┘ ┴┴ └────
doc └─────┘ └──┘└───┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
txt └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
par └─────┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
pid └───┘└┘ └──┘ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └────
st ─────────────────────────────────────────────────────────────────────────────────────────────────────────────
202 exists_lt_of_cInf_lt (range_nonempty _) (by rw [infi]; linarith),
id └──────────────────┘ └────────────┘ └──┘
src ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
typ ─────┘└──────────────────┘┴ └────────────┘└──┘ ┴└──┘└──┘┴└┘└──────┘┴
doc ─────┘└──────────────────┘┴ └──┘ ┴└──┘└──┘┴└┘└──────┘┴
txt ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
par ─────┘ ┴ └──┘ ┴└──┘ ┴└┘└──────┘┴
pid ─────┘ ┴ └──┘ └───┘ └──────────┘
st ────────────────────────────────────────────────┘└───────┘┴└────────┘┴└─
203 rcases this with ⟨b, brange, hb⟩,
id └──┘
src └─────┘ └───────────────────┘
typ └─────┘└──┘└───────────────────┘
doc └─────┘ └───────────────────┘
txt └─────┘ └───────────────────┘
par └─────┘ └───────────────────┘
pid ┴ └───────────────────┘
st ───────────────────────────────────┘└─
204 rcases mem_range.1 brange with ⟨q, qb⟩,
id └───────┘ └────┘
src └─────┘└───────┘└─┘ └───────────┘
typ └─────┘└───────┘└─┘└────┘└───────────┘
doc └─────┘ └─┘ └───────────┘
txt └─────┘ └─┘ └───────────┘
par └─────┘ └─┘ └───────────┘
pid ┴ └─┘ └───────────┘
st ─────────────────────────────────────────┘└─
205 rw ← qb at hb,
id └┘
src └───┘ └────┘
typ └───┘└┘└────┘
doc └───┘ └────┘
txt └───┘ └────┘
par └───┘ └────┘
pid └─┘ └────┘
st ────────────────┘└─
206 have : dist (Ψ p) (Ψ q) ≤ dist (Φ p) (Φ q) + 2 * ε,
id ┴ └──┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ └┘ ┴ └┘ ┴└──┘┴ ┴ └┘ ┴ └┘ └─┘ ┴
typ └─────┘ ┴ ┴ └┘ ┴┴ └┘ ┴└──┘┴ ┴┴└┘ ┴┴┴└┘ └─┘ ┴┴
doc └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
txt └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
par └─────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
pid └───┘└┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ └┘ ┴ └┘ └─┘ ┴
st ─────────────────────────────────────────────────────┘└─
207 { have := le_trans (neg_le_abs_self _) (H p q), by linarith },
id └──────┘ └─────────────┘ ┴ ┴ ┴
src └──────┘└──────┘┴ └─────────────┘└──┘ ┴ ┴ ┴ └───────┘
typ └──────┘└──────┘┴ └─────────────┘└──┘ ┴┴┴┴┴┴ └───────┘
doc └──────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘
txt └──────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘
par └──────┘ ┴ └──┘ ┴ ┴ ┴ └───────┘
pid └───┘└─┘ ┴ └──┘ ┴ ┴ ┴ ┴
st ───────┘└──────────────────────────────────────────┘ └┘└
208 calc dist x z ≤ dist x (Ψ p) + dist (Ψ p) (Ψ q) + dist (Ψ q) z : dist_triangle4 _ _ _ _
id └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └────────────┘
src └──┘ └──┘ └────────────┘
typ └──┘ ┴ ┴ └──┘ ┴ ┴ ┴ └────────────┘
doc └──┘
st ────────────────────────────────────────────────────────────────────────────────────────────
209 ... ≤ dist x (Ψ p) + dist (Φ p) (Φ q) + dist z (Ψ q) + 2 * ε : by rw [dist_comm z]; linarith
id ┴ ┴ └───────┘ ┴
src └──┘└───────┘┴ ┴ └────────
typ ┴ ┴ └──┘└───────┘┴┴┴ └────────
doc └──┘ ┴ ┴ └────────
txt └──┘ ┴ ┴ └────────
par └──┘ ┴ ┴ └────────
pid └┘ ┴ ┴ └
st ──────────────────────────────────────────────────────────────────────┘└──────────────┘┴└──────────
210 ... ≤ dist x (Ψ p) + (dist y (Φ p) + dist y (Φ q)) + dist z (Ψ q) + 2 * ε :
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘└───────────────────────────────────────────────────────────────────────────
211 add_le_add (add_le_add (add_le_add (le_refl _) (dist_triangle_left _ _ _)) (le_refl _)) (le_refl _)
id └────────┘ └────────────────┘ └─────┘
src └────────┘ └────────────────┘ └─────┘
typ └────────┘ └────────────────┘ └─────┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────────────
212 ... ≤ (infi (λp, dist y (Φ p) + dist x (Ψ p)) + ε) + (infi (λp, dist y (Φ p) + dist z (Ψ p)) + ε) + δ :
id ┴ └──┘ ┴ ┴ ┴
src └──┘
typ ┴ └──┘ ┴ ┴ ┴
doc └──┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
213 by linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────┘└─────────
214 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
215
216 private lemma glue_eq_of_dist_eq_zero (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) (ε0 : 0 < ε) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
217 ∀p q : α ⊕ β, glue_dist Φ Ψ ε p q = 0 → p = q
id ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
218 | (inl x) (inl y) h := by rw eq_of_dist_eq_zero h
id └─┘ └────────────────┘ ┴
src └─┘ └─┘└────────────────┘┴ ┴
typ └─┘ └─┘└────────────────┘┴┴┴
doc └─┘ ┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st └───────────────────────┘
219 | (inl x) (inr y) h := begin
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
st └─────
220 have : 0 ≤ infi (λp, dist x (Φ p) + dist y (Ψ p)) :=
id ┴ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └───────┘┴┴└──┘┴ └─┘ ┴ ┴ ┴ └┘┴┴└──┘┴ ┴ ┴ └─────
typ └───────┘┴┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘┴┴└──┘┴┴┴ ┴┴ └─────
doc └───────┘ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────
txt └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────
par └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────
pid └───┘└──┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘└───
st ─────────────────────────────────────────────────────────
221 le_cinfi (λp, by simpa using add_le_add (@dist_nonneg _ _ x _) (@dist_nonneg _ _ y _)),
id └──────┘ └────────┘ ┴ └─────────┘ ┴
src ─────┘└──────┘┴ └─┘ ┴└──────────┘└────────┘┴ └───┘ └──┘ └─────────┘└───┘ └─┘┴
typ ─────┘└──────┘┴ └─┘ ┴└──────────┘└────────┘┴ └───┘┴└──┘ └─────────┘└───┘┴└─┘┴
doc ─────┘└──────┘┴ └─┘ ┴└──────────┘ ┴ └───┘ └──┘ └───┘ └─┘┴
txt ─────┘ ┴ └─┘ ┴└──────────┘ ┴ └───┘ └──┘ └───┘ └─┘┴
par ─────┘ ┴ └─┘ ┴└──────────┘ ┴ └───┘ └──┘ └───┘ └─┘┴
pid ─────┘ ┴ └─┘ └───────────┘ ┴ └───┘ └──┘ └───┘ └──┘
st ─────────────────────┘└───────────────────────────────────────────────────────────────────┘┴└─
222 have : 0 + ε ≤ glue_dist Φ Ψ ε (inl x) (inr y) := add_le_add this (le_refl ε),
id └───────┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └────────┘ └──┘ └─────┘ ┴
src └───────┘ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ └─┘┴ └┘ └─┘┴ └───┘└────────┘┴ ┴ └─────┘┴ ┴
typ └───────┘ ┴ ┴ ┴└───────┘┴┴┴┴┴┴┴ └─┘┴┴└┘ └─┘┴┴└───┘└────────┘┴└──┘┴ └─────┘┴┴┴
doc └───────┘ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
pid └───┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
223 exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ──────────┘└─
224 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────
225 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
226 | (inr x) (inl y) h := begin
id └─┘ └─┘
src └─┘ └─┘
typ └─┘ └─┘
st └─────
227 have : 0 ≤ infi (λp, dist y (Φ p) + dist x (Ψ p)) :=
id └──┘ ┴ ┴ └──┘ ┴ ┴
src └───────┘ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴└──┘┴ ┴ ┴ └─────
typ └───────┘ ┴└──┘┴ └─┘ ┴┴┴ ┴┴ └┘ ┴└──┘┴┴┴ ┴┴ └─────
doc └───────┘ ┴└──┘┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────
txt └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────
par └───────┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─────
pid └───┘└──┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘└───
st ─────────────────────────────────────────────────────────
228 le_cinfi (λp, by simpa using add_le_add (@dist_nonneg _ _ x _) (@dist_nonneg _ _ y _)),
id └──────┘ └────────┘ ┴ └─────────┘ ┴
src ─────┘└──────┘┴ └─┘ ┴└──────────┘└────────┘┴ └───┘ └──┘ └─────────┘└───┘ └─┘┴
typ ─────┘└──────┘┴ └─┘ ┴└──────────┘└────────┘┴ └───┘┴└──┘ └─────────┘└───┘┴└─┘┴
doc ─────┘└──────┘┴ └─┘ ┴└──────────┘ ┴ └───┘ └──┘ └───┘ └─┘┴
txt ─────┘ ┴ └─┘ ┴└──────────┘ ┴ └───┘ └──┘ └───┘ └─┘┴
par ─────┘ ┴ └─┘ ┴└──────────┘ ┴ └───┘ └──┘ └───┘ └─┘┴
pid ─────┘ ┴ └─┘ └───────────┘ ┴ └───┘ └──┘ └───┘ └──┘
st ─────────────────────┘└───────────────────────────────────────────────────────────────────┘┴└─
229 have : 0 + ε ≤ glue_dist Φ Ψ ε (inr x) (inl y) := add_le_add this (le_refl ε),
id └───────┘ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ └────────┘ └──┘ └─────┘ ┴
src └───────┘ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ └─┘┴ └┘ └─┘┴ └───┘└────────┘┴ ┴ └─────┘┴ ┴
typ └───────┘ ┴ ┴ ┴└───────┘┴┴┴┴┴┴┴ └─┘┴┴└┘ └─┘┴┴└───┘└────────┘┴└──┘┴ └─────┘┴┴┴
doc └───────┘ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └───┘ ┴ ┴ ┴ ┴
pid └───┘└──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────────────────────────────────┘└─
230 exfalso,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
st ──────────┘└─
231 linarith
src └────────
typ └────────
doc └────────
txt └────────
par └────────
pid └
st ─────────────
232 end
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
233 | (inr x) (inr y) h := by rw eq_of_dist_eq_zero h
id └─┘ └────────────────┘ ┴
src └─┘ └─┘└────────────────┘┴ └
typ └─┘ └─┘└────────────────┘┴┴└
doc └─┘ ┴ └
txt └─┘ ┴ └
par └─┘ ┴ └
pid ┴ ┴ └
st └────────────────────────
234
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
235 /-- Given two maps Φ and Ψ intro metric spaces α and β such that the distances between Φ p and Φ q,
236 and between Ψ p and Ψ q, coincide up to 2 ε where ε > 0, one can almost glue the two spaces α
237 and β along the images of Φ and Ψ, so that Φ p and Ψ p are at distance ε. -/
238 def glue_metric_approx (Φ : γ → α) (Ψ : γ → β) (ε : ℝ) (ε0 : 0 < ε)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
239 (H : ∀p q, abs (dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)) ≤ 2 * ε) : metric_space (α ⊕ β) :=
id ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
src └─┘ └──┘ ┴ └──┘ ┴ ┴ └──────────┘ ┴
typ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──────────┘ ┴ ┴ ┴
doc └──────────┘
240 { dist := glue_dist Φ Ψ ε,
id ┴ └───────┘ ┴ ┴ ┴
src ┴ └───────┘
typ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘
241 dist_self := glue_dist_self Φ Ψ ε,
id └────────────┘ ┴ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴ ┴
242 dist_comm := glue_dist_comm Φ Ψ ε,
id └────────────┘ ┴ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴ ┴
243 dist_triangle := glue_dist_triangle Φ Ψ ε H,
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴
244 eq_of_dist_eq_zero := glue_eq_of_dist_eq_zero Φ Ψ ε ε0 }
id └─────────────────────┘ ┴ ┴ ┴ └┘
src └─────────────────────┘
typ └─────────────────────┘ ┴ ┴ ┴ └┘
245
246 end approx_gluing
247
248 section sum
249 /- A particular case of the previous construction is when one uses basepoints in α and β and one
250 glues only along the basepoints, putting them at distance 1. We give a direct definition of
251 the distance, without infi, as it is easier to use in applications, and show that it is equal to
252 the gluing distance defined above to take advantage of the lemmas we have already proved. -/
253
254 variables [metric_space α] [metric_space β] [inhabited α] [inhabited β]
id └──────────┘ └──────────┘ └───────┘ └───────┘
src └──────────┘ └──────────┘ └───────┘ └───────┘
typ └──────────┘ └──────────┘ └───────┘ └───────┘
doc └──────────┘ └──────────┘
255 open sum (inl inr)
256
257 /- Distance on a disjoint union. There are many (noncanonical) ways to put a distance compatible
258 with each factor.
259 If the two spaces are bounded, one can say for instance that each point in the first is at distance
260 `diam α + diam β + 1` of each point in the second.
261 Instead, we choose a construction that works for unbounded spaces, but requires basepoints.
262 We embed isometrically each factor, set the basepoints at distance 1,
263 arbitrarily, and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
264 their respective basepoints, plus the distance 1 between the basepoints.
265 Since there is an arbitrary choice in this construction, it is not an instance by default. -/
266
267 def sum.dist : α ⊕ β → α ⊕ β → ℝ
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
268 | (inl a) (inl a') := dist a a'
id ┴ └─┘ └┘ └──┘
src └─┘ └──┘
typ ┴ └─┘ └┘ └──┘
269 | (inr b) (inr b') := dist b b'
id ┴ └─┘ └┘ └──┘
src └─┘ └──┘
typ ┴ └─┘ └┘ └──┘
270 | (inl a) (inr b) := dist a (default α) + 1 + dist (default β) b
id └─┘ ┴ └─┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴
src └─┘ └─┘ └──┘ └─────┘ ┴ ┴ └──┘ └─────┘
typ └─┘ ┴ └─┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴
271 | (inr b) (inl a) := dist b (default β) + 1 + dist (default α) a
id └─┘ ┴ └─┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴
src └─┘ └─┘ └──┘ └─────┘ ┴ ┴ └──┘ └─────┘
typ └─┘ ┴ └─┘ ┴ └──┘ └─────┘ ┴ ┴ ┴ └──┘ └─────┘ ┴
272
273 lemma sum.dist_eq_glue_dist {p q : α ⊕ β} :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
274 sum.dist p q = glue_dist (λ_ : unit, default α) (λ_ : unit, default β) 1 p q :=
id └──────┘ ┴ ┴ ┴ └───────┘ └──┘ └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴
src └──────┘ ┴ └───────┘ └──┘ └─────┘ └──┘ └─────┘
typ └──────┘ ┴ ┴ ┴ └───────┘ └──┘ └─────┘ ┴ └──┘ └─────┘ ┴ ┴ ┴
doc └───────┘ └──┘ └──┘
275 by cases p; cases q; refl <|> simp [sum.dist, glue_dist, dist_comm]
id ┴ ┴ └──────┘ └───────┘ └───────┘
src └────┘ └────┘ └───┘ └────┘└──────┘└┘└───────┘└┘└───────┘└─
typ └────┘┴ └────┘┴ └───┘ └────┘└──────┘└┘└───────┘└┘└───────┘└─
doc └────┘ └────┘ └───┘ └────┘ └┘└───────┘└┘ └─
txt └────┘ └────┘ └───┘ └────┘ └┘ └┘ └─
par └────┘ └────┘ └───┘ └────┘ └┘ └┘ └─
pid ┴ ┴ ┴ ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────────
276
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
277 private lemma sum.dist_comm (x y : α ⊕ β) : sum.dist x y = sum.dist y x :=
id ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src ┴ └──────┘ ┴ └──────┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
278 by cases x; cases y; simp only [sum.dist, dist_comm, add_comm, add_left_comm]
id ┴ ┴ └──────┘ └───────┘ └──────┘ └───────────┘
src └────┘ └────┘ └─────────┘└──────┘└┘└───────┘└┘└──────┘└┘└───────────┘└─
typ └────┘┴ └────┘┴ └─────────┘└──────┘└┘└───────┘└┘└──────┘└┘└───────────┘└─
doc └────┘ └────┘ └─────────┘ └┘ └┘ └┘ └─
txt └────┘ └────┘ └─────────┘ └┘ └┘ └┘ └─
par └────┘ └────┘ └─────────┘ └┘ └┘ └┘ └─
pid ┴ ┴ ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────
279
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
280 lemma sum.one_dist_le {x : α} {y : β} : 1 ≤ sum.dist (inl x) (inr y) :=
id ┴ ┴ ┴ └──────┘ └─┘ ┴ └─┘ ┴
src ┴ └──────┘ └─┘ └─┘
typ ┴ ┴ ┴ └──────┘ └─┘ ┴ └─┘ ┴
281 le_trans (le_add_of_nonneg_right dist_nonneg) $
id └──────┘ └────────────────────┘ └─────────┘
src └──────┘ └────────────────────┘ └─────────┘
typ └──────┘ └────────────────────┘ └─────────┘
282 add_le_add_right (le_add_of_nonneg_left dist_nonneg) _
id └──────────────┘ └───────────────────┘ └─────────┘
src └──────────────┘ └───────────────────┘ └─────────┘
typ └──────────────┘ └───────────────────┘ └─────────┘
283
284 lemma sum.one_dist_le' {x : α} {y : β} : 1 ≤ sum.dist (inr y) (inl x) :=
id ┴ ┴ ┴ └──────┘ └─┘ ┴ └─┘ ┴
src ┴ └──────┘ └─┘ └─┘
typ ┴ ┴ ┴ └──────┘ └─┘ ┴ └─┘ ┴
285 by rw sum.dist_comm; exact sum.one_dist_le
id └───────────┘ └─────────────┘
src └─┘└───────────┘ └────┘└─────────────┘└
typ └─┘└───────────┘ └────┘└─────────────┘└
doc └─┘ └────┘ └
txt └─┘ └────┘ └
par └─┘ └────┘ └
pid ┴ ┴ └
st └────────────────────────────────────────
286
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
287 private lemma sum.mem_uniformity (s : set ((α ⊕ β) × (α ⊕ β))) :
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
288 s ∈ (@uniformity (α ⊕ β) _).sets ↔ ∃ ε > 0, ∀ a b, sum.dist a b < ε → (a, b) ∈ s :=
id ┴ ┴ └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src ┴ └────────┘ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
typ ┴ ┴ └────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └────────┘
289 begin
st └─────
290 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
291 { rintro ⟨hsα, hsβ⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ───┘└───────────────┘└─
292 rcases mem_uniformity_dist.1 hsα with ⟨εα, εα0, hα⟩,
id └─────────────────┘ └─┘
src └─────┘└─────────────────┘└─┘ └─────────────────┘
typ └─────┘└─────────────────┘└─┘└─┘└─────────────────┘
doc └─────┘ └─┘ └─────────────────┘
txt └─────┘ └─┘ └─────────────────┘
par └─────┘ └─┘ └─────────────────┘
pid ┴ └─┘ └─────────────────┘
st ──────────────────────────────────────────────────────┘└─
293 rcases mem_uniformity_dist.1 hsβ with ⟨εβ, εβ0, hβ⟩,
id └─────────────────┘ └─┘
src └─────┘└─────────────────┘└─┘ └─────────────────┘
typ └─────┘└─────────────────┘└─┘└─┘└─────────────────┘
doc └─────┘ └─┘ └─────────────────┘
txt └─────┘ └─┘ └─────────────────┘
par └─────┘ └─┘ └─────────────────┘
pid ┴ └─┘ └─────────────────┘
st ──────────────────────────────────────────────────────┘└─
294 refine ⟨min (min εα εβ) 1, lt_min (lt_min εα0 εβ0) zero_lt_one, _⟩,
id └─┘ └┘ └┘ └────┘ └─┘ └─┘ └─────────┘
src └─────┘ ┴ └─┘┴ ┴ └───┘ ┴ └────┘┴ ┴ └┘└─────────┘└──┘
typ └─────┘ ┴ └─┘┴└┘┴└┘└───┘ ┴ └────┘┴└─┘┴└─┘└┘└─────────┘└──┘
doc └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └──┘
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └──┘
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └──┘
pid ┴ ┴ ┴ ┴ └───┘ ┴ ┴ ┴ └┘ └──┘
st ─────────────────────────────────────────────────────────────────────┘└─
295 rintro (a|a) (b|b) h,
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
txt └──────────────────┘
par └──────────────────┘
pid └────────────┘
st ───────────────────────┘└─
296 { exact hα (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_left _ _))) },
id └┘ └────────────┘ ┴ └──────┘ └─────────┘
src └────┘ ┴ └────────────┘┴ ┴ └──────┘┴ └────┘ └─────────┘└──────┘
typ └────┘└┘┴ └────────────┘┴┴┴ └──────┘┴ └────┘ └─────────┘└──────┘
doc └────┘ ┴ ┴ ┴ ┴ └────┘ └──────┘
txt └────┘ ┴ ┴ ┴ ┴ └────┘ └──────┘
par └────┘ ┴ ┴ ┴ ┴ └────┘ └──────┘
pid ┴ ┴ ┴ ┴ ┴ └────┘ └─────┘┴
st ─────┘└─────────────────────────────────────────────────────────────────────────┘└┘└
297 { cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) sum.one_dist_le },
id └──────────┘ └────────────┘ ┴ └──────────┘ └─────────────┘
src └────┘└──────────┘┴ └────────────┘┴ ┴ └──────────┘└─────┘└─────────────┘┴
typ └────┘└──────────┘┴ └────────────┘┴┴┴ └──────────┘└─────┘└─────────────┘┴
doc └────┘ ┴ ┴ ┴ └─────┘ ┴
txt └────┘ ┴ ┴ ┴ └─────┘ ┴
par └────┘ ┴ ┴ ┴ └─────┘ ┴
pid ┴ ┴ ┴ ┴ └─────┘ ┴
st ─────┘└───────────────────────────────────────────────────────────────────────┘└┘└
298 { cases not_le_of_lt (lt_of_lt_of_le h (min_le_right _ _)) sum.one_dist_le' },
id └──────────┘ └────────────┘ ┴ └──────────┘ └──────────────┘
src └────┘└──────────┘┴ └────────────┘┴ ┴ └──────────┘└─────┘└──────────────┘┴
typ └────┘└──────────┘┴ └────────────┘┴┴┴ └──────────┘└─────┘└──────────────┘┴
doc └────┘ ┴ ┴ ┴ └─────┘ ┴
txt └────┘ ┴ ┴ ┴ └─────┘ ┴
par └────┘ ┴ ┴ ┴ └─────┘ ┴
pid ┴ ┴ ┴ ┴ └─────┘ ┴
st ─────┘└────────────────────────────────────────────────────────────────────────┘└┘└
299 { exact hβ (lt_of_lt_of_le h (le_trans (min_le_left _ _) (min_le_right _ _))) } },
id └┘ └────────────┘ ┴ └──────┘ └─────────┘ └──────────┘
src └────┘ ┴ └────────────┘┴ ┴ └──────┘┴ └─────────┘└────┘ └──────────┘└──────┘
typ └────┘└┘┴ └────────────┘┴┴┴ └──────┘┴ └─────────┘└────┘ └──────────┘└──────┘
doc └────┘ ┴ ┴ ┴ ┴ └────┘ └──────┘
txt └────┘ ┴ ┴ ┴ ┴ └────┘ └──────┘
par └────┘ ┴ ┴ ┴ ┴ └────┘ └──────┘
pid ┴ ┴ ┴ ┴ ┴ └────┘ └─────┘┴
st ─────────────────────────────────────────────────────────────────────────────────┘└──┘└
300 { rintro ⟨ε, ε0, H⟩,
src └───────────────┘
typ └───────────────┘
doc └───────────────┘
txt └───────────────┘
par └───────────────┘
pid └─────────┘
st ────────────────────┘└─
301 split; rw [filter.mem_map, mem_uniformity_dist];
id └────────────┘ └─────────────────┘
src └───┘ └──┘└────────────┘└┘└─────────────────┘┴
typ └───┘ └──┘└────────────┘└┘└─────────────────┘┴
doc └───┘ └──┘ └┘ ┴
txt └───┘ └──┘ └┘ ┴
par └───┘ └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────┘└────────────┘└───────────────────┘┴└─
302 exact ⟨ε, ε0, λ x y h, H _ _ (by exact h)⟩ }
id ┴ └┘ ┴ ┴
src └────┘ └┘ └┘ └──────┘ └───┘ └─────┘ └─┘
typ └────┘ ┴└┘└┘└┘ └──────┘┴└───┘ └─────┘┴└─┘
doc └────┘ └┘ └┘ └──────┘ └───┘ └─────┘ └─┘
txt └────┘ └┘ └┘ └──────┘ └───┘ └─────┘ └─┘
par └────┘ └┘ └┘ └──────┘ └───┘ └─────┘ └─┘
pid ┴ └┘ └┘ └──────┘ └───┘ └─────┘ └┘┴
st ─────────────────────────────────────┘└──────┘└─┘└─
303 end
st ──┘
304
305 /-- The distance on the disjoint union indeed defines a metric space. All the distance properties follow from our
306 choice of the distance. The harder work is to show that the uniform structure defined by the distance coincides
307 with the disjoint union uniform structure. -/
308 def metric_space_sum : metric_space (α ⊕ β) :=
id └──────────┘ ┴ ┴ ┴
src └──────────┘ ┴
typ └──────────┘ ┴ ┴ ┴
doc └──────────┘
309 { dist := sum.dist,
id ┴ └──────┘
src ┴ └──────┘
typ ┴ └──────┘
310 dist_self := λx, by cases x; simp only [sum.dist, dist_self],
id ┴ ┴ └──────┘ └───────┘
src └────┘ └─────────┘└──────┘└┘└───────┘┴
typ ┴ └────┘┴ └─────────┘└──────┘└┘└───────┘┴
doc └────┘ └─────────┘ └┘ ┴
txt └────┘ └─────────┘ └┘ ┴
par └────┘ └─────────┘ └┘ ┴
pid ┴ ┴└──┘└┘ └┘ ┴
st └───────────────────────────────────────┘
311 dist_comm := sum.dist_comm,
id └───────────┘
src └───────────┘
typ └───────────┘
312 dist_triangle := λp q r,
id ┴ ┴ ┴
typ ┴ ┴ ┴
313 by simp only [dist, sum.dist_eq_glue_dist]; exact glue_dist_triangle _ _ _ (by simp; norm_num) _ _ _,
id └───────────────────┘ └────────────────┘
src └─────────┘ └┘└───────────────────┘┴ └────┘└────────────────┘└─────┘ ┴└──┘└┘└──────┘└─────┘
typ └─────────┘ └┘└───────────────────┘┴ └────┘└────────────────┘└─────┘ ┴└──┘└┘└──────┘└─────┘
doc └─────────┘ └┘ ┴ └────┘ └─────┘ ┴└──┘└┘└──────┘└─────┘
txt └─────────┘ └┘ ┴ └────┘ └─────┘ ┴└──┘└┘└──────┘└─────┘
par └─────────┘ └┘ ┴ └────┘ └─────┘ ┴└──┘└┘└──────┘└─────┘
pid ┴└──┘└┘ └┘ ┴ ┴ └─────┘ └────────────────────┘
st └──────────────────────────────────────────────────────────────────────────┘└─────────────┘└─────┘
314 eq_of_dist_eq_zero := λp q,
id ┴ ┴
typ ┴ ┴
315 by simp only [dist, sum.dist_eq_glue_dist]; exact glue_eq_of_dist_eq_zero _ _ _ zero_lt_one _ _,
id └───────────────────┘ └─────────────────────┘ └─────────┘
src └─────────┘ └┘└───────────────────┘┴ └────┘└─────────────────────┘└─────┘└─────────┘└──┘
typ └─────────┘ └┘└───────────────────┘┴ └────┘└─────────────────────┘└─────┘└─────────┘└──┘
doc └─────────┘ └┘ ┴ └────┘ └─────┘ └──┘
txt └─────────┘ └┘ ┴ └────┘ └─────┘ └──┘
par └─────────┘ └┘ ┴ └────┘ └─────┘ └──┘
pid ┴└──┘└┘ └┘ ┴ ┴ └─────┘ └──┘
st └───────────────────────────────────────────────────────────────────────────────────────────┘
316 to_uniform_space := sum.uniform_space,
id └───────────────┘
src └───────────────┘
typ └───────────────┘
317 uniformity_dist := uniformity_dist_of_mem_uniformity _ _ sum.mem_uniformity }
id └───────────────────────────────┘ └────────────────┘
src └───────────────────────────────┘ └────────────────┘
typ └───────────────────────────────┘ └────────────────┘
doc └───────────────────────────────┘
318
319 local attribute [instance] metric_space_sum
id └──────────────┘
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
320
321 lemma sum.dist_eq {x y : α ⊕ β} : dist x y = sum.dist x y := rfl
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘
src ┴ └──┘ ┴ └──────┘ └─┘
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └─┘
322
323 /-- The left injection of a space in a disjoint union in an isometry -/
324 lemma isometry_on_inl : isometry (sum.inl : α → (α ⊕ β)) :=
id └──────┘ └─────┘ ┴ ┴ ┴ ┴
src └──────┘ └─────┘ ┴
typ └──────┘ └─────┘ ┴ ┴ ┴ ┴
doc └──────┘
325 isometry_emetric_iff_metric.2 $ λx y, rfl
id └─────────────────────────┘┴ ┴ ┴ └─┘
src └─────────────────────────┘┴ └─┘
typ └─────────────────────────┘┴ ┴ ┴ └─┘
doc └─────────────────────────┘
326
327 /-- The right injection of a space in a disjoint union in an isometry -/
328 lemma isometry_on_inr : isometry (sum.inr : β → (α ⊕ β)) :=
id └──────┘ └─────┘ ┴ ┴ ┴ ┴
src └──────┘ └─────┘ ┴
typ └──────┘ └─────┘ ┴ ┴ ┴ ┴
doc └──────┘
329 isometry_emetric_iff_metric.2 $ λx y, rfl
id └─────────────────────────┘┴ ┴ ┴ └─┘
src └─────────────────────────┘┴ └─┘
typ └─────────────────────────┘┴ ┴ ┴ └─┘
doc └─────────────────────────┘
330
331 end sum
332
333 section gluing
334 /- Exact gluing of two metric spaces along isometric subsets. -/
335
336 variables [nonempty γ] [metric_space γ] [metric_space α] [metric_space β]
id └──────┘ └──────────┘ └──────────┘ └──────────┘
src └──────┘ └──────────┘ └──────────┘ └──────────┘
typ └──────┘ └──────────┘ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘ └──────────┘
337 {Φ : γ → α} {Ψ : γ → β} {ε : ℝ}
id ┴
src ┴
typ ┴
338 open sum (inl inr)
339 local attribute [instance] premetric.dist_setoid
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
doc └───────────────────┘
340
341 def glue_premetric (hΦ : isometry Φ) (hΨ : isometry Ψ) : premetric_space (α ⊕ β) :=
id └──────┘ ┴ └──────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └──────┘ └──────┘ └─────────────┘ ┴
typ └──────┘ ┴ └──────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └──────┘ └──────┘
342 { dist := glue_dist Φ Ψ 0,
id └───────┘ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴
doc └───────┘
343 dist_self := glue_dist_self Φ Ψ 0,
id └────────────┘ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴
344 dist_comm := glue_dist_comm Φ Ψ 0,
id └────────────┘ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴
345 dist_triangle := glue_dist_triangle Φ Ψ 0 $ λp q, by rw [hΦ.dist_eq, hΨ.dist_eq]; simp }
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ └──┘ └┘ ┴ └───┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └──┘└────────┘└┘└────────┘┴ └───┘
doc └──┘ └┘ ┴ └───┘
txt └──┘ └┘ ┴ └───┘
par └──┘ └┘ ┴ └───┘
pid └┘ └┘ ┴ ┴
st └─────────────┘└──────────┘┴└─────┘
346
347 def glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) : Type* :=
id └──────┘ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ └──────┘ ┴
doc └──────┘ └──────┘
348 @metric_quot _ (glue_premetric hΦ hΨ)
id └─────────┘ └────────────┘ └┘ └┘
src └─────────┘ └────────────┘
typ └─────────┘ └────────────┘ └┘ └┘
doc └─────────┘
349
350 instance metric_space_glue_space (hΦ : isometry Φ) (hΨ : isometry Ψ) :
id └──────┘ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ └──────┘ ┴
doc └──────┘ └──────┘
351 metric_space (glue_space hΦ hΨ) :=
id └──────────┘ └────────┘ └┘ └┘
src └──────────┘ └────────┘
typ └──────────┘ └────────┘ └┘ └┘
doc └──────────┘
352 @premetric.metric_space_quot _ (glue_premetric hΦ hΨ)
id └─────────────────────────┘ └────────────┘ └┘ └┘
src └─────────────────────────┘ └────────────┘
typ └─────────────────────────┘ └────────────┘ └┘ └┘
353
354 def to_glue_l (hΦ : isometry Φ) (hΨ : isometry Ψ) (x : α) : glue_space hΦ hΨ :=
id └──────┘ ┴ └──────┘ ┴ ┴ └────────┘ └┘ └┘
src └──────┘ └──────┘ └────────┘
typ └──────┘ ┴ └──────┘ ┴ ┴ └────────┘ └┘ └┘
doc └──────┘ └──────┘
355 by letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inl x⟧
id └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ └┘ ┴└─┘ ┴┴
src └─────┘└─────────────┘┴ ┴┴┴ └───┘└────────────┘┴ ┴ └────┘┴└─┘┴ ┴└
typ └─────┘└─────────────┘┴ ┴┴┴┴┴└───┘└────────────┘┴└┘┴└┘ └────┘┴└─┘┴┴┴└
doc └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴ └
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴ └
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴ └
pid ┴└┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────────────────────
356
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
357 def to_glue_r (hΦ : isometry Φ) (hΨ : isometry Ψ) (y : β) : glue_space hΦ hΨ :=
id └──────┘ ┴ └──────┘ ┴ ┴ └────────┘ └┘ └┘
src └──────┘ └──────┘ └────────┘
typ └──────┘ ┴ └──────┘ ┴ ┴ └────────┘ └┘ └┘
doc └──────┘ └──────┘
358 by letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ; exact ⟦inr y⟧
id └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ └┘ ┴└─┘ ┴┴
src └─────┘└─────────────┘┴ ┴┴┴ └───┘└────────────┘┴ ┴ └────┘┴└─┘┴ ┴└
typ └─────┘└─────────────┘┴ ┴┴┴┴┴└───┘└────────────┘┴└┘┴└┘ └────┘┴└─┘┴┴┴└
doc └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴ └
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴ └
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └────┘ ┴ └
pid ┴└┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────────────────────
359
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
360 instance inhabited_left (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited α] :
id └──────┘ ┴ └──────┘ ┴ └───────┘ ┴
src └──────┘ └──────┘ └───────┘
typ └──────┘ ┴ └──────┘ ┴ └───────┘ ┴
doc └──────┘ └──────┘
361 inhabited (glue_space hΦ hΨ) :=
id └───────┘ └────────┘ └┘ └┘
src └───────┘ └────────┘
typ └───────┘ └────────┘ └┘ └┘
362 ⟨to_glue_l _ _ (default _)⟩
id └───────┘ └─────┘
src └───────┘ └─────┘
typ └───────┘ └─────┘
363
364 instance inhabited_right (hΦ : isometry Φ) (hΨ : isometry Ψ) [inhabited β] :
id └──────┘ ┴ └──────┘ ┴ └───────┘ ┴
src └──────┘ └──────┘ └───────┘
typ └──────┘ ┴ └──────┘ ┴ └───────┘ ┴
doc └──────┘ └──────┘
365 inhabited (glue_space hΦ hΨ) :=
id └───────┘ └────────┘ └┘ └┘
src └───────┘ └────────┘
typ └───────┘ └────────┘ └┘ └┘
366 ⟨to_glue_r _ _ (default _)⟩
id └───────┘ └─────┘
src └───────┘ └─────┘
typ └───────┘ └─────┘
367
368 lemma to_glue_commute (hΦ : isometry Φ) (hΨ : isometry Ψ) :
id └──────┘ ┴ └──────┘ ┴
src └──────┘ └──────┘
typ └──────┘ ┴ └──────┘ ┴
doc └──────┘ └──────┘
369 (to_glue_l hΦ hΨ) ∘ Φ = (to_glue_r hΦ hΨ) ∘ Ψ :=
id └───────┘ └┘ └┘ ┴ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴
src └───────┘ ┴ ┴ └───────┘ ┴
typ └───────┘ └┘ └┘ ┴ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴
370 begin
st └─────
371 letI : premetric_space (α ⊕ β) := glue_premetric hΦ hΨ,
id └─────────────┘ ┴ ┴ ┴ └────────────┘ └┘ └┘
src └─────┘└─────────────┘┴ ┴┴┴ └───┘└────────────┘┴ ┴
typ └─────┘└─────────────┘┴ ┴┴┴┴┴└───┘└────────────┘┴└┘┴└┘
doc └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴
txt └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴
par └─────┘ ┴ ┴ ┴ └───┘ ┴ ┴
pid ┴└┘ ┴ ┴ ┴ ┴└──┘ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
372 funext,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
373 simp only [comp, to_glue_l, to_glue_r, quotient.eq],
id └──┘ └───────┘ └───────┘ └─────────┘
src └─────────┘└──┘└┘└───────┘└┘└───────┘└┘└─────────┘┴
typ └─────────┘└──┘└┘└───────┘└┘└───────┘└┘└─────────┘┴
doc └─────────┘ └┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────┘└─
374 exact glue_dist_glued_points Φ Ψ 0 x
id └────────────────────┘ ┴ ┴ ┴
src └────┘└────────────────────┘┴ ┴ └─┘ ┴
typ └────┘└────────────────────┘┴┴┴┴└─┘┴┴
doc └────┘ ┴ ┴ └─┘ ┴
txt └────┘ ┴ ┴ └─┘ ┴
par └────┘ ┴ ┴ └─┘ ┴
pid ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────┘
375 end
st └─┘
376
377 lemma to_glue_l_isometry (hΦ : isometry Φ) (hΨ : isometry Ψ) : isometry (to_glue_l hΦ hΨ) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ └───────┘ └┘ └┘
src └──────┘ └──────┘ └──────┘ └───────┘
typ └──────┘ ┴ └──────┘ ┴ └──────┘ └───────┘ └┘ └┘
doc └──────┘ └──────┘ └──────┘
378 isometry_emetric_iff_metric.2 $ λ_ _, rfl
id └─────────────────────────┘┴ ┴ ┴ └─┘
src └─────────────────────────┘┴ └─┘
typ └─────────────────────────┘┴ ┴ ┴ └─┘
doc └─────────────────────────┘
379
380 lemma to_glue_r_isometry (hΦ : isometry Φ) (hΨ : isometry Ψ) : isometry (to_glue_r hΦ hΨ) :=
id └──────┘ ┴ └──────┘ ┴ └──────┘ └───────┘ └┘ └┘
src └──────┘ └──────┘ └──────┘ └───────┘
typ └──────┘ ┴ └──────┘ ┴ └──────┘ └───────┘ └┘ └┘
doc └──────┘ └──────┘ └──────┘
381 isometry_emetric_iff_metric.2 $ λ_ _, rfl
id └─────────────────────────┘┴ ┴ ┴ └─┘
src └─────────────────────────┘┴ └─┘
typ └─────────────────────────┘┴ ┴ ┴ └─┘
doc └─────────────────────────┘
382
383 end gluing --section
384
385 section inductive_limit
386 /- In this section, we define the inductive limit of
387 f 0 f 1 f 2 f 3
388 X 0 -----> X 1 -----> X 2 -----> X 3 -----> ...
389 where the X n are metric spaces and f n isometric embeddings. We do it by defining a premetric
390 space structure on Σn, X n, where the predistance dist x y is obtained by pushing x and y in a
391 common X k using composition by the f n, and taking the distance there. This does not depend on
392 the choice of k as the f n are isometries. The metric space associated to this premetric space
393 is the desired inductive limit.-/
394 open nat
395
396 variables {X : ℕ → Type u} [∀n, metric_space (X n)] {f : Πn, X n → X (n+1)}
id ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴┴
src ┴ └──────────┘ ┴
typ ┴ ┴ └──────────┘ ┴ ┴ ┴ ┴ ┴┴
doc └──────────┘
397
398 /-- Predistance on the disjoint union Σn, X n. -/
399 def inductive_limit_dist (f : Πn, X n → X (n+1)) (x y : Σn, X n) : ℝ :=
id ┴ ┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴┴ ┴┴┴ ┴ ┴ ┴
400 dist (le_rec_on (le_max_left x.1 y.1) f x.2 : X (max x.1 y.1))
id └──┘ └───────┘ └─────────┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └─┘ ┴┴ ┴┴
src └──┘ └───────┘ └─────────┘ ┴ ┴ ┴ └─┘ ┴ ┴
typ └──┘ └───────┘ └─────────┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └─┘ ┴┴ ┴┴
doc └───────┘
401 (le_rec_on (le_max_right x.1 y.1) f y.2 : X (max x.1 y.1))
id └───────┘ └──────────┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └─┘ ┴┴ ┴┴
src └───────┘ └──────────┘ ┴ ┴ ┴ └─┘ ┴ ┴
typ └───────┘ └──────────┘ ┴┴ ┴┴ ┴ ┴┴ ┴ └─┘ ┴┴ ┴┴
doc └───────┘
402
403 /-- The predistance on the disjoint union Σn, X n can be computed in any X k for large enough k.-/
404 lemma inductive_limit_dist_eq_dist (I : ∀n, isometry (f n))
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
405 (x y : Σn, X n) (m : ℕ) : ∀hx : x.1 ≤ m, ∀hy : y.1 ≤ m,
id ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴┴┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ ┴ ┴
406 inductive_limit_dist f x y = dist (le_rec_on hx f x.2 : X m) (le_rec_on hy f y.2 : X m) :=
id └──────────────────┘ ┴ ┴ ┴ ┴ └──┘ └───────┘ └┘ ┴ ┴┴ ┴ ┴ └───────┘ └┘ ┴ ┴┴ ┴ ┴
src └──────────────────┘ ┴ └──┘ └───────┘ ┴ └───────┘ ┴
typ └──────────────────┘ ┴ ┴ ┴ ┴ └──┘ └───────┘ └┘ ┴ ┴┴ ┴ ┴ └───────┘ └┘ ┴ ┴┴ ┴ ┴
doc └──────────────────┘ └───────┘ └───────┘
407 begin
st └─────
408 induction m with m hm,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
409 { assume hx hy,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───┘└──────────┘└─
410 have A : max x.1 y.1 = 0, { rw [le_zero_iff_eq.1 hx, le_zero_iff_eq.1 hy], simp },
id └─┘ ┴ ┴ ┴ └────────────┘ └┘ └────────────┘ └┘
src └───────┘└─┘┴ └─┘ └─┘┴└┘ └──┘└────────────┘└─┘ └┘└────────────┘└─┘ ┴ └───┘
typ └───────┘└─┘┴┴└─┘┴└─┘┴└┘ └──┘└────────────┘└─┘└┘└┘└────────────┘└─┘└┘┴ └───┘
doc └───────┘ ┴ └─┘ └─┘ └┘ └──┘ └─┘ └┘ └─┘ ┴ └───┘
txt └───────┘ ┴ └─┘ └─┘ └┘ └──┘ └─┘ └┘ └─┘ ┴ └───┘
par └───────┘ ┴ └─┘ └─┘ └┘ └──┘ └─┘ └┘ └─┘ ┴ └───┘
pid └────┘└─┘ ┴ └─┘ └─┘ ┴┴ └┘ └─┘ └┘ └─┘ ┴ ┴
st ───────────────────────────┘└──┘└─────────────────────┘└───────────────────┘└──────┘└┘└
411 unfold inductive_limit_dist,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └───────────────────┘
st ──────────────────────────────┘└─
412 congr; simp only [A] },
id ┴
src └───┘ └─────────┘ └┘
typ └───┘ └─────────┘┴└┘
doc └─────────┘ └┘
txt └───┘ └─────────┘ └┘
par └───┘ └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st ────────────────────────┘└┘└
413 { assume hx hy,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid └──────────┘
st ───────────────┘└─
414 by_cases h : max x.1 y.1 = m.succ,
id └─┘ ┴ ┴ └────┘
src └───────┘ └─┘└─┘┴ └─┘ └─┘ ┴└────┘
typ └───────┘ └─┘└─┘┴┴└─┘┴└─┘ ┴└────┘
doc └───────┘ └─┘ ┴ └─┘ └─┘ ┴
txt └───────┘ └─┘ ┴ └─┘ └─┘ ┴
par └───────┘ └─┘ ┴ └─┘ └─┘ ┴
pid ┴ └─┘ ┴ └─┘ └─┘ ┴
st ────────────────────────────────────┘└─
415 { unfold inductive_limit_dist,
src └─────────────────────────┘
typ └─────────────────────────┘
doc └─────────────────────────┘
txt └─────────────────────────┘
par └─────────────────────────┘
pid └───────────────────┘
st ─────┘└─────────────────────────┘└─
416 congr; simp only [h] },
id ┴
src └───┘ └─────────┘ └┘
typ └───┘ └─────────┘┴└┘
doc └─────────┘ └┘
txt └───┘ └─────────┘ └┘
par └───┘ └─────────┘ └┘
pid ┴└──┘└┘ ┴┴
st ──────────────────────────┘└┘└
417 { have : max x.1 y.1 ≤ succ m := by simp [hx, hy],
id └─┘ ┴ ┴ ┴ └──┘ ┴ └┘ └┘
src └─────┘└─┘┴ └─┘ └─┘┴┴└──┘┴ └──┘ ┴└────┘ └┘ ┴
typ └─────┘└─┘┴┴└─┘┴└─┘┴┴└──┘┴┴└──┘ ┴└────┘└┘└┘└┘┴
doc └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴└────┘ └┘ ┴
txt └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴└────┘ └┘ ┴
par └─────┘ ┴ └─┘ └─┘ ┴ ┴ └──┘ ┴└────┘ └┘ ┴
pid └───┘└┘ ┴ └─┘ └─┘ ┴ ┴ └──┘ └─────┘ └┘ ┴
st ──────────────────────────────────────┘└────────────┘└─
418 have : max x.1 y.1 ≤ m := by simpa [h] using of_le_succ this,
id └─┘ ┴ ┴ ┴ ┴ └────────┘ └──┘
src └─────┘└─┘┴ └─┘ └─┘ ┴ └──┘ ┴└─────┘ └──────┘└────────┘┴
typ └─────┘└─┘┴┴└─┘┴└─┘ ┴┴└──┘ ┴└─────┘┴└──────┘└────────┘┴└──┘
doc └─────┘ ┴ └─┘ └─┘ ┴ └──┘ ┴└─────┘ └──────┘ ┴
txt └─────┘ ┴ └─┘ └─┘ ┴ └──┘ ┴└─────┘ └──────┘ ┴
par └─────┘ ┴ └─┘ └─┘ ┴ └──┘ ┴└─────┘ └──────┘ ┴
pid └───┘└┘ ┴ └─┘ └─┘ ┴ └──┘ └──────┘ └──────┘ ┴
st ─────────────────────────────────┘└──────────────────────────────┘└─
419 have xm : x.1 ≤ m := le_trans (le_max_left _ _) this,
id ┴ ┴ └──────┘ └─────────┘ └──┘
src └────────┘ └─┘ ┴ └──┘└──────┘┴ └─────────┘└────┘
typ └────────┘┴└─┘ ┴┴└──┘└──────┘┴ └─────────┘└────┘└──┘
doc └────────┘ └─┘ ┴ └──┘ ┴ └────┘
txt └────────┘ └─┘ ┴ └──┘ ┴ └────┘
par └────────┘ └─┘ ┴ └──┘ ┴ └────┘
pid └─────┘└─┘ └─┘ ┴ └──┘ ┴ └────┘
st ─────────────────────────────────────────────────────────┘└─
420 have ym : y.1 ≤ m := le_trans (le_max_right _ _) this,
id ┴ ┴ └──────┘ └──────────┘ └──┘
src └────────┘ └─┘ ┴ └──┘└──────┘┴ └──────────┘└────┘
typ └────────┘┴└─┘ ┴┴└──┘└──────┘┴ └──────────┘└────┘└──┘
doc └────────┘ └─┘ ┴ └──┘ ┴ └────┘
txt └────────┘ └─┘ ┴ └──┘ ┴ └────┘
par └────────┘ └─┘ ┴ └──┘ ┴ └────┘
pid └─────┘└─┘ └─┘ ┴ └──┘ ┴ └────┘
st ──────────────────────────────────────────────────────────┘└─
421 rw [le_rec_on_succ xm, le_rec_on_succ ym, (I m).dist_eq],
id └────────────┘ └┘ └────────────┘ └┘ ┴ ┴
src └──┘└────────────┘┴ └┘└────────────┘┴ └┘ ┴ └────────┘
typ └──┘└────────────┘┴└┘└┘└────────────┘┴└┘└┘ ┴┴┴└────────┘
doc └──┘ ┴ └┘ ┴ └┘ ┴ └────────┘
txt └──┘ ┴ └┘ ┴ └┘ ┴ └────────┘
par └──┘ ┴ └┘ ┴ └┘ ┴ └────────┘
pid └┘ ┴ └┘ ┴ └┘ ┴ └────────┘
st ──────────────────────────┘└─────────────────┘└────────────┘└───
422 exact hm xm ym }}
id └┘ └┘ └┘
src └────┘ ┴ ┴ ┴
typ └────┘└┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ────────────────────┘└──
423 end
st ──┘
424
425 /-- Premetric space structure on Σn, X n.-/
426 def inductive_premetric (I : ∀n, isometry (f n)) :
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
427 premetric_space (Σn, X n) :=
id └─────────────┘ ┴┴┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴┴┴ ┴ ┴
428 { dist := inductive_limit_dist f,
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
doc └──────────────────┘
429 dist_self := λx, by simp [dist, inductive_limit_dist],
id ┴ └──────────────────┘
src └────┘ └┘└──────────────────┘┴
typ ┴ └────┘ └┘└──────────────────┘┴
doc └────┘ └┘└──────────────────┘┴
txt └────┘ └┘ ┴
par └────┘ └┘ ┴
pid ┴┴ └┘ ┴
st └────────────────────────────────┘
430 dist_comm := λx y, begin
id ┴ ┴
typ ┴ ┴
st └─────
431 let m := max x.1 y.1,
id └─┘ ┴ ┴
src └───────┘└─┘┴ └─┘ └┘
typ └───────┘└─┘┴┴└─┘┴└┘
doc └───────┘ ┴ └─┘ └┘
txt └───────┘ ┴ └─┘ └┘
par └───────┘ ┴ └─┘ └┘
pid └───┘┴└─┘ ┴ └─┘ └┘
st ───────────────────────┘└─
432 have hx : x.1 ≤ m := le_max_left _ _,
id ┴ ┴ ┴ └─────────┘
src └────────┘ └─┘┴┴ └──┘└─────────┘└──┘
typ └────────┘┴└─┘┴┴┴└──┘└─────────┘└──┘
doc └────────┘ └─┘ ┴ └──┘ └──┘
txt └────────┘ └─┘ ┴ └──┘ └──┘
par └────────┘ └─┘ ┴ └──┘ └──┘
pid └─────┘└─┘ └─┘ ┴ └──┘ └──┘
st ───────────────────────────────────────┘└─
433 have hy : y.1 ≤ m := le_max_right _ _,
id ┴ ┴ └──────────┘
src └────────┘ └─┘ ┴ └──┘└──────────┘└──┘
typ └────────┘┴└─┘ ┴┴└──┘└──────────┘└──┘
doc └────────┘ └─┘ ┴ └──┘ └──┘
txt └────────┘ └─┘ ┴ └──┘ └──┘
par └────────┘ └─┘ ┴ └──┘ └──┘
pid └─────┘└─┘ └─┘ ┴ └──┘ └──┘
st ────────────────────────────────────────┘└─
434 unfold dist,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
435 rw [inductive_limit_dist_eq_dist I x y m hx hy, inductive_limit_dist_eq_dist I y x m hy hx,
id └──────────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘ └──────────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘
src └──┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
typ └──┘└──────────────────────────┘┴┴┴┴┴┴┴┴┴└┘┴└┘└┘└──────────────────────────┘┴┴┴┴┴┴┴┴┴└┘┴└┘└─
doc └──┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
txt └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ─────────────────────────────────────────────────┘└──────────────────────────────────────────┘└─
436 dist_comm]
id └───────┘
src ───────┘└───────┘└─
typ ───────┘└───────┘└─
doc ───────┘ └─
txt ───────┘ └─
par ───────┘ └─
pid ───────┘ ┴└
st ────────────────┘┴└
437 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
438 dist_triangle := λx y z, begin
id ┴ ┴ ┴
typ ┴ ┴ ┴
st └─────
439 let m := max (max x.1 y.1) z.1,
id └─┘ ┴ ┴ ┴
src └───────┘ ┴ └─┘┴ └─┘ └──┘ └┘
typ └───────┘ ┴ └─┘┴┴└─┘┴└──┘┴└┘
doc └───────┘ ┴ ┴ └─┘ └──┘ └┘
txt └───────┘ ┴ ┴ └─┘ └──┘ └┘
par └───────┘ ┴ ┴ └─┘ └──┘ └┘
pid └───┘┴└─┘ ┴ ┴ └─┘ └──┘ └┘
st ─────────────────────────────────┘└─
440 have hx : x.1 ≤ m := le_trans (le_max_left _ _) (le_max_left _ _),
id ┴ ┴ └──────┘ └─────────┘
src └────────┘ └─┘ ┴ └──┘└──────┘┴ └────┘ └─────────┘└───┘
typ └────────┘┴└─┘ ┴┴└──┘└──────┘┴ └────┘ └─────────┘└───┘
doc └────────┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
txt └────────┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
par └────────┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
pid └─────┘└─┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
st ────────────────────────────────────────────────────────────────────┘└─
441 have hy : y.1 ≤ m := le_trans (le_max_right _ _) (le_max_left _ _),
id ┴ ┴ └──────┘ └──────────┘ └─────────┘
src └────────┘ └─┘ ┴ └──┘└──────┘┴ └──────────┘└────┘ └─────────┘└───┘
typ └────────┘┴└─┘ ┴┴└──┘└──────┘┴ └──────────┘└────┘ └─────────┘└───┘
doc └────────┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
txt └────────┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
par └────────┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
pid └─────┘└─┘ └─┘ ┴ └──┘ ┴ └────┘ └───┘
st ─────────────────────────────────────────────────────────────────────┘└─
442 have hz : z.1 ≤ m := le_max_right _ _,
id ┴ ┴ └──────────┘
src └────────┘ └─┘ ┴ └──┘└──────────┘└──┘
typ └────────┘┴└─┘ ┴┴└──┘└──────────┘└──┘
doc └────────┘ └─┘ ┴ └──┘ └──┘
txt └────────┘ └─┘ ┴ └──┘ └──┘
par └────────┘ └─┘ ┴ └──┘ └──┘
pid └─────┘└─┘ └─┘ ┴ └──┘ └──┘
st ────────────────────────────────────────┘└─
443 calc inductive_limit_dist f x z
id └──┘
src └──┘
typ └──┘
doc └──┘
st ────────────────────────────────────
444 = dist (le_rec_on hx f x.2 : X m) (le_rec_on hz f z.2 : X m) :
id └──┘ └───────┘ ┴ ┴
src └──┘ └───────┘
typ └──┘ └───────┘ ┴ ┴
doc └───────┘
st ─────────────────────────────────────────────────────────────────────
445 inductive_limit_dist_eq_dist I x z m hx hz
id └──────────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘
src └──────────────────────────┘
typ └──────────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘
doc └──────────────────────────┘
st ───────────────────────────────────────────────────
446 ... ≤ dist (le_rec_on hx f x.2 : X m) (le_rec_on hy f y.2 : X m)
id ┴ ┴
src ┴ ┴
typ ┴ ┴
st ───────────────────────────────────────────────────────────────────────
447 + dist (le_rec_on hy f y.2 : X m) (le_rec_on hz f z.2 : X m) :
id ┴ └┘ ┴
src ┴ ┴
typ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────────────
448 dist_triangle _ _ _
id └───────────┘
src └───────────┘
typ └───────────┘
st ────────────────────────────
449 ... = inductive_limit_dist f x y + inductive_limit_dist f y z :
id └──────────────────┘ ┴
src └──────────────────┘
typ └──────────────────┘ ┴
doc └──────────────────┘
st ──────────────────────────────────────────────────────────────────────
450 by rw [inductive_limit_dist_eq_dist I x y m hx hy,
id └──────────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘
src └──┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
typ └──┘└──────────────────────────┘┴┴┴┴┴┴┴┴┴└┘┴└┘└─
doc └──┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
txt └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid └┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
st ──────────┘└─────────────────────────────────────────────┘└─
451 inductive_limit_dist_eq_dist I y z m hy hz]
id └──────────────────────────┘ ┴ ┴ ┴ ┴ └┘ └┘
src ───────────────┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
typ ───────────────┘└──────────────────────────┘┴┴┴┴┴┴┴┴┴└┘┴└┘└─
doc ───────────────┘└──────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─
txt ───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
par ───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─
pid ───────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴└
st ─────────────────────────────────────────────────────────┘┴└
452 end }
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
453
454 local attribute [instance] inductive_premetric premetric.dist_setoid
id └─────────────────┘ └───────────────────┘
src └─────────────────┘ └───────────────────┘
typ └─────────────────┘ └───────────────────┘
doc └─────────────────┘ └───────────────────┘
455
456 /-- The type giving the inductive limit in a metric space context. -/
457 def inductive_limit (I : ∀n, isometry (f n)) : Type* :=
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
458 @metric_quot _ (inductive_premetric I)
id └─────────┘ └─────────────────┘ ┴
src └─────────┘ └─────────────────┘
typ └─────────┘ └─────────────────┘ ┴
doc └─────────┘ └─────────────────┘
459
460 /-- Metric space structure on the inductive limit. -/
461 instance metric_space_inductive_limit (I : ∀n, isometry (f n)) :
id ┴ └──────┘ ┴ ┴
src └──────┘
typ ┴ └──────┘ ┴ ┴
doc └──────┘
462 metric_space (inductive_limit I) :=
id └──────────┘ └─────────────┘ ┴
src └──────────┘ └─────────────┘
typ └──────────┘ └─────────────┘ ┴
doc └──────────┘ └─────────────┘
463 @premetric.metric_space_quot _ (inductive_premetric I)
id └─────────────────────────┘ └─────────────────┘ ┴
src └─────────────────────────┘ └─────────────────┘
typ └─────────────────────────┘ └─────────────────┘ ┴
doc └─────────────────┘
464
465 /-- Mapping each `X n` to the inductive limit. -/
466 def to_inductive_limit (I : ∀n, isometry (f n)) (n : ℕ) (x : X n) : metric.inductive_limit I :=
id ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴
src └──────┘ ┴ └────────────────────┘
typ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴
doc └──────┘ └────────────────────┘
467 by letI : premetric_space (Σn, X n) := inductive_premetric I; exact ⟦sigma.mk n x⟧
id └─────────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴└──────┘ ┴ ┴┴
src └─────┘└─────────────┘┴ ┴┴┴┴ ┴ └───┘└─────────────────┘┴ └────┘┴└──────┘┴ ┴ ┴└
typ └─────┘└─────────────┘┴ ┴┴┴┴┴┴ └───┘└─────────────────┘┴┴ └────┘┴└──────┘┴┴┴┴┴└
doc └─────┘ ┴ ┴ ┴ ┴ └───┘└─────────────────┘┴ └────┘ ┴ ┴ └
txt └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ └
par └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ ┴ └
pid ┴└┘ ┴ ┴ ┴ ┴ ┴└──┘ ┴ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────────────────────────
468
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
469 instance (I : ∀ n, isometry (f n)) [inhabited (X 0)] : inhabited (inductive_limit I) :=
id ┴ └──────┘ ┴ ┴ └───────┘ ┴ └───────┘ └─────────────┘ ┴
src └──────┘ └───────┘ └───────┘ └─────────────┘
typ ┴ └──────┘ ┴ ┴ └───────┘ ┴ └───────┘ └─────────────┘ ┴
doc └──────┘ └─────────────┘
470 ⟨to_inductive_limit _ 0 (default _)⟩
id └────────────────┘ └─────┘
src └────────────────┘ └─────┘
typ └────────────────┘ └─────┘
doc └────────────────┘
471
472 /-- The map `to_inductive_limit n` mapping `X n` to the inductive limit is an isometry. -/
473 lemma to_inductive_limit_isometry (I : ∀n, isometry (f n)) (n : ℕ) :
id ┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
474 isometry (to_inductive_limit I n) := isometry_emetric_iff_metric.2 $ λx y,
id └──────┘ └────────────────┘ ┴ ┴ └─────────────────────────┘┴ ┴ ┴
src └──────┘ └────────────────┘ └─────────────────────────┘┴
typ └──────┘ └────────────────┘ ┴ ┴ └─────────────────────────┘┴ ┴ ┴
doc └──────┘ └────────────────┘ └─────────────────────────┘
475 begin
st └─────
476 change inductive_limit_dist f ⟨n, x⟩ ⟨n, y⟩ = dist x y,
id └──────────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └─────┘└──────────────────┘┴ ┴ └┘ └┘ └┘ └┘┴┴└──┘┴ ┴
typ └─────┘└──────────────────┘┴┴┴ └┘ └┘ ┴└┘ └┘┴┴└──┘┴┴┴┴
doc └─────┘└──────────────────┘┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
txt └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
pid ┴ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ ┴
st ───────────────────────────────────────────────────────┘└─
477 rw [inductive_limit_dist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n),
id └──────────────────────────┘ ┴ ┴ ┴ └─────┘ ┴
src └──┘└──────────────────────────┘┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ └─────┘┴ └──
typ └──┘└──────────────────────────┘┴┴┴ └┘┴└┘ └┘┴└┘ ┴ ┴ └┘ └─────┘┴┴└──
doc └──┘└──────────────────────────┘┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴ └──
txt └──┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴ └──
par └──┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴ └──
pid └┘ ┴ ┴ └┘ └┘ └┘ └┘ ┴ ┴ └┘ ┴ └──
st ───────────────────────────────────────────────────────────────────────────┘└─
478 le_rec_on_self, le_rec_on_self]
id └────────────┘ └────────────┘
src ─────┘└────────────┘└┘└────────────┘└┘
typ ─────┘└────────────┘└┘└────────────┘└┘
doc ─────┘ └┘ └┘
txt ─────┘ └┘ └┘
par ─────┘ └┘ └┘
pid ─────┘ └┘ ┴┴
st ───────────────────┘└──────────────┘┴┴
479 end
st └─┘
480
481 /-- The maps `to_inductive_limit n` are compatible with the maps `f n`. -/
482 lemma to_inductive_limit_commute (I : ∀n, isometry (f n)) (n : ℕ) :
id ┴ └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
483 (to_inductive_limit I n.succ) ∘ (f n) = to_inductive_limit I n :=
id └────────────────┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴
src └────────────────┘ └───┘ ┴ ┴ └────────────────┘
typ └────────────────┘ ┴ ┴└───┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘
484 begin
st └─────
485 funext,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
st ───────┘└─
486 simp only [comp, to_inductive_limit, quotient.eq],
id └──┘ └────────────────┘ └─────────┘
src └─────────┘└──┘└┘└────────────────┘└┘└─────────┘┴
typ └─────────┘└──┘└┘└────────────────┘└┘└─────────┘┴
doc └─────────┘ └┘└────────────────┘└┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ──────────────────────────────────────────────────┘└─
487 show inductive_limit_dist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0,
id └──────────────────┘ └────┘ ┴ ┴ ┴ ┴
src └───┘└──────────────────┘┴ ┴ └────┘└┘ ┴ ┴ └┘ └┘ └┘┴└┘
typ └───┘└──────────────────┘┴ ┴ └────┘└┘┴┴ ┴ └┘ ┴└┘┴└┘┴└┘
doc └───┘└──────────────────┘┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘
txt └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘
par └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └┘
pid └───┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ ┴┴
st ───────────────────────────────────────────────────────┘└─
488 { rw [inductive_limit_dist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ,
id └──────────────────────────┘ ┴ ┴ ┴ └────┘
src └──┘└──────────────────────────┘┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘└────┘└─
typ └──┘└──────────────────────────┘┴┴┴ └┘┴┴ ┴ └┘ └┘┴└┘└────┘└─
doc └──┘└──────────────────────────┘┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └─
txt └──┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └─
par └──┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └─
pid └┘ ┴ ┴ └┘ ┴ ┴ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────┘└─
489 le_rec_on_self, le_rec_on_succ, le_rec_on_self, dist_self],
id └────────────┘ └────────────┘ └────────────┘ └───────┘
src ───────┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘┴
typ ───────┘└────────────┘└┘└────────────┘└┘└────────────┘└┘└───────┘┴
doc ───────┘ └┘ └┘ └┘ ┴
txt ───────┘ └┘ └┘ └┘ ┴
par ───────┘ └┘ └┘ └┘ ┴
pid ───────┘ └┘ └┘ └┘ ┴
st ─────────────────────┘└──────────────┘└──────────────┘└─────────┘└──
490 exact le_refl _,
id └─────┘
src └────┘└─────┘└┘
typ └────┘└─────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ──────────────────┘└─
491 exact le_refl _,
id └─────┘
src └────┘└─────┘└┘
typ └────┘└─────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ──────────────────┘└─
492 exact le_succ _ }
id └─────┘
src └────┘└─────┘└─┘
typ └────┘└─────┘└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └┘┴
st ───────────────────┘└─
493 end
st ──┘
494
495 end inductive_limit --section
496 end metric --namespace